perm filename AFOSR.TXT[PAR,SYS] blob
sn#551592 filedate 1980-12-18 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00034 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00004 00002 .device xgp
C00025 00003 .s Abstract
C00031 00004 .S Overview and Relevance
C00039 00005 .S Guide to Reading
C00040 00006 .S INTRODUCTION TO GENERAL THEORY
C00043 00007 .SS Approach
C00045 00008 .SS Program Synthesis Context
C00049 00009 .SS Summary of Previous Work
C00052 00010 .SS Program Synthesis Phase
C00062 00011 .SS Existing Synthesis Rules
C00063 00012 .SSS Rules for a List-to-List Insertion Sort
C00078 00013 .SSS Rules for an In-Place Insertion Sort
C00087 00014 .S |RESEARCH PROBLEM: CONCURRENT PROGRAMS|
C00088 00015 .SS Research Plan
C00093 00016 .SS Codification of Program Synthesis Knowledge
C00099 00017 .SS Specification of Concurrent Programs and Systems
C00104 00018 .SS Specification of Target Machines
C00105 00019 .SS Target Tasks to Focus Research
C00193 00020 .S QUALIFICATIONS OF PERSONNEL
C00196 00021 .S REFERENCES
C00230 00022 .S |PERSONNEL|
C00231 00023 .SS |Cordell Green, Chief Scientist, Computer Science|
C00234 00024 .SSS |Research Summary|
C00256 00025 .SS |David C. Luckham, Consultant|
C00266 00026 .SS |Jorge V. Phillips, Computer Scientist|
C00279 00027 .SS |Stephen J. Westfold, Research Assistant|
C00282 00028 .S COMPUTER FACILITIES
C00287 00029 .S COMPANY BACKGROUND
C00290 00030 .S CURRENT AND PENDING SUPPORT
C00293 00031 .S GENERAL BIBLIOGRAPHY
C00304 00032 .APP RESULTS IN KNOWLEDGE BASED PROGRAM SYNTHESIS
C00305 00033 .APP EFFICIENCY EXPERT
C00310 00034 .APP |ON PROGRAM SYNTHESIS KNOWLEDGE|
C00312 ENDMK
C⊗;
.device xgp
.
. << FONT DEFINITIONS >>
.
. << To use nonie fonts do as follows (default is times roman)
. .nonm←true
. .require .....
. >>
.
.if declaration(nonm) then
. start
. font 1 "nonm" << 12 point nonie >>
. font 2 "nonmi" << 12 point nonie for italics >>
. font 3 "nonmb" << 12 point nonie bold >>
. end
.else
. start
. font 1 "tim12s" << 12 point sail times >>
. font 2 "tim12i" << 12 point times for italics >>
. font 3 "tim12b" << 12 point times bold >>
. end;
.font 4 "tim10b" << times roman bold 10pt para headers >>
.font 5 "nonsup[fnt,jp]"
.font 6 "nonsub[fnt,jp]" << para subindices >>
.font 7 "grfxs1[fnt,jp]" << para graficas >>
.font 8 "timfix[fnt,jp]" << para ejemplos >>
.font 9 "fix20" << para footnotes >>
.font A "metlb" << para titulos >>
.font B "grkb30" << para griego >>
.font C "math[fnt,jp]" << bullets >>
.font D "tim10r" << para abstract >>
.font E "tim10i" << para acknowledgement >>
.
.turn on "{α%↓_#"
.at "//" TXT "/" ⊂ lastfont2 ← thisfont; ("%2TXT%" & lastfont2) ⊃
.at "⊗⊗" TXT "⊗" ⊂ lastfont3 ← thisfont; ("%3TXT%" & lastfont3) ⊃
.at "\\" TXT "\" ⊂ lastfont4 ← thisfont; ("%4TXT%" & lastfont4) ⊃
.at "↑↑" TXT "↑" ⊂ lastfont5 ← thisfont; ("%5TXT%" & lastfont5) ⊃
.at "↓↓" TXT "↓" ⊂ lastfont6 ← thisfont; ("%6TXT%" & lastfont6) ⊃
.at "[[" TXT "]" ⊂ lastfont8 ← thisfont; ("%8TXT%" & lastfont8) ⊃
.at "++" TXT "+" ⊂ lastfont8 ← thisfont; ("%8TXT%" & lastfont8) ⊃
.at "≡OM≡" ⊂ lastfontb ← thisfont; ("%BW%" & lastfontb) ⊃
.at "≡U" ⊂ "%3User:%*" ⊃ << user >>
.at "≡S" ⊂ "%3CHI:%*" ⊃ << system >>
.
.
. << escapes para fonts >>
.
.macro nfnt ⊂ select 1 ⊃; << normal font >>
.macro itfnt ⊂ select 2 ⊃; << normal italics font >>
.macro it ⊂ select 2 ⊃; << para compatibilidad >>
.macro boldfnt ⊂ select 3 ⊃; << normal bold font >>
.
.macro smitfnt ⊂ select E ⊃; << small italics times font >>
.macro smbofnt ⊂ select 4 ⊃; << small bold times font >>
.
.macro titfnt ⊂ select A ⊃;
.macro upfnt ⊂ select 5 ⊃;
.macro grfxfnt ⊂ select 7 ⊃;
.macro fixfnt ⊂ select 8 ⊃;
.macro footfnt ⊂ select 9 ⊃;
.macro tinyfnt ⊂ select 9 ⊃;
.macro grkfnt ⊂ select B ⊃; << greek selector >>
. << PAGE FRAME DEFINITIONS >>
.
.macro setspacing(n)
. ⊂
. spacing n mills; << intraline in mills >>
. mainspacing ← millspacing; << save it for justify macro >>
. ⊃
.
.<< note: there are 200 pixels per inch on the xgp, so vbpi = hbpi = 200.
. there are 5 mills per pixel, or 1000 mills per inch.
. there are 2.8 pixels per point, or 14 mills per point.
.
. normal interline spacing for a 30 pixel font is 3 pixels or 15 mills
. double spacing would be 33*2-30=36 pixels or 180 mills
. 1 1/2 spacing, 1.5*33-30 pixels or 100 mills >>
.
.setspacing(70)
.
.sline ← 165; << line height in mills for single space,
. 30 pixel font>>
.nline ← 15; << normal millspacing for 30 pixel font >>
.cskip ← 165; << number of mills to skip before chapters in table
. of contents >>
.sskip ← 15; << number of mills for spacing of sections in table
. of contents>>
.
. << paper size and margination macros >>
.
.macro paper_size (x,y) ⊂ mill_paper_height ← y;
. mill_paper_width ← x; ⊃
.
.variable page_height, page_width
.
.macro margins (εleft,εright,εtop,εbottom)
. ⊂
. start
. nfnt; << normal font >>
. if declaration(nonm) then charw←14;
. if mill_paper_height ≤ 0
. then mill_paper_height ← 11000; << 8.5" x 11" default >>
. if mill_paper_width ≤ 0
. then mill_paper_width ← 8500;
.
. bit_raster_width ← (mill_paper_width*hbpi)/1000;
. bit_raster_height ← (mill_paper_height*vbpi)/1000;
.
. << set up margins according to parameters >>
. if left ≥ 0 then oddleftborder ← left else oddleftborder ← 1500;
. if right ≥ 0 then rightborder ← right else rightborder ← 1000;
. if top ≥ 0 then topborder ← top else topborder ← 1000;
. if bottom ≥ 0 then bottomborder ← bottom else bottomborder ← 500;
.
. evenleftborder ← oddleftborder;
. xgp_vsp ← (millspacing*vbpi)/1000;
.
. page_width ← (bit_raster_width-
. (hbpi*(oddleftborder+rightborder))/1000)/charw
. linewidth ← page_width; << for some macros like caja >>
. page_height← (bit_raster_height -
. (vbpi*(topborder+bottomborder))/1000) / (charh+xgp_vsp);
.
.
. << set up the page frame >>
. page frame page_width wide page_height high;
. area text lines 4 to page_height-3;
. title area heading lines 1 to 3;
. title area footing lines page_height-3;
. place text;
.
. << for use in book format: omitted! >>
. << area text lines 3 to page_height-2>>
. << title area footing line page_height>>
. end
. ⊃;
.
.
.point←14 <<for 12 point fonts >>;
.macro pt2 ⊂skip 2*point mills⊃
.macro pt18 ⊂skip 6*point mills⊃
.macro pt24 ⊂skip 12*point mills⊃
. << DEFAULT FLAGS >>
.
.hascontents ← false; << default no contents table >>
.rosa ← false << rosa requirements >>
.indentenormal ← false; << no indente 4 espacios cada parrafo default >>
. << PAGE, NORMAL, FOOTNOTE MACROS >>
.
.count page from 1 to 888;
.
.macro fac ⊂ fill; adjust; compact; ⊃
.
.macro normal ⊂
. fac
. preface 1;
. if rosa then
. start double space end
. else start spacing mainspacing mills; end;
. << normally use 65 mills for papers etc. >>
. << some of the memos where typude using 100 mills >>
. if indentenormal
. then start indent 4,0,0; end
. else start indent 0,0,0; end;
.
. select 1
. ⊃
.
. << Footnote macros >>
.
.footsep ← "----------"
.count footnote inline printing "%51%*"
.
.at "$$$" TXT "$" ⊂
. next footnote;
{footnote!}
. send foot
. ⊂ begin
. fill;
. turn on "{" << just in case >>
. preface 1;
. spacing 0;
. indent 0,0,0;
. footfnt; << Font chiquito >>
{footnote!} txt
. end;
. ⊃
. ⊃
.
.macro code
. ⊂
. skip; << Must quote % here! >>
. begin nofill; indent 5,5; fixfnt; group;
. ⊃
.
.macro mcode << codigo chiquito >>
. ⊂
. skip; << Must quote % here! >>
. begin nofill; indent 5,5; select 9;
. ⊃
.
.macro exind (n)
. ⊂ skip;
. once indent n,n; nofill; fixfnt; turn off "{";
. ⊃
.
.macro bind (n) << para indentar bloques de ejemplos. Requiere END >>
. ⊂
. begin indent n,n; nofill; fixfnt; turn off "{"; skip 1; group
. ⊃
.
. << Spacing and Dialogue macros >>
.
.macro sp (n) << to set spacing to some number of mills >>
. ⊂ spacing n mills ⊃
.
.macro p (n) << to set preface to some number of mills >>
. ⊂ preface n mills ⊃
.
.macro spp(n,m) << to set spacing and preface in mills >>
. ⊂ sp n; p m; ⊃
.
.macro dial << for dialogue in times roman >>
. ⊂
. if lines<4 then next page else skip;
. begin "dial"
. indent 5,11;spp(30,80)
. ⊃;
.
.macro dialc
. ⊂
. skip;
. begin "dialcomment"
. indent 5,5; spp(30,80)
. ⊃
.
.macro endc
. ⊂
. end "dialcomment";
. ⊃
.
.macro endd
. ⊂
. end "dial";
. ⊃
.
.macro scenario
. ⊂
. begin nfnt; indent 5,5; spp 30,80;
. ⊃
.
.macro itscenario
. ⊂
. begin itfnt; indent 5,5,5; spp 30,80
. ⊃
. << Section macros: S, SS, SSS, SSSS, FIG, CB, REFERENCES >>
.
.count seccion
.
.macro s (titulo)
. ⊂
. if lines<7 then skip to column 1 else skip;
. next seccion
. every heading (\\titulo\,,\\{PAGE}\)
. if hascontents then
. send contents
. ⊂
. checkskip;
. skip 1;
{seccion!}. titulo→{page!}
. ⊃;
. once boldfnt; turn on "↓_"; <<not centering any more >>
. indent 0,0,0;
{seccion!}. titulo
. normal
. ⊃
.
.count subseccion in seccion printing "!.1"
.
.macro ss (titulo)
. ⊂
. if lines<6 then skip to column 1 else skip 2;
. next subseccion
. once nofill; flush left; select 3
{subseccion!} titulo
. if hascontents then
. send contents
. ⊂
. checkskip;
{subseccion!}. titulo→{page!}
. ⊃
. normal
. ⊃
.
.count subsub in subseccion printing "!.1"
.
.macro sss (titulo)
. ⊂
. if lines<7 then skip to column 1 else skip ;
. next subsub
. once nofill; flush left; boldfnt;
{subsub!} titulo
. if hascontents then
. send contents
. ⊂
. checkskip;
{subsub!}. titulo→{page!}
. ⊃
. normal
. ⊃
.count subsubsub in subsub printing "!.1"
.
.macro ssss (titulo)
. ⊂
. if lines<7 then skip to column 1 else skip;
. next subsubsub
. once nofill; flush left; boldfnt;
{subsubsub!}. titulo
. if hascontents then
. send contents
. ⊂
. checkskip;
{subsubsub!}. titulo→{page!}
. ⊃
. normal
. ⊃
.
.count figura in seccion printing "!.1"
.
.macro fig (titulo)
. ⊂
. skip 1
. Next figura
. once nofill; center; smbofnt;
Fig. {figura!} titulo
. normal
. ⊃
.
.macro cb (titulo) << subtitulo sin seccionamiento >>
. ⊂
. if lines<10 then skip to column 1 else skip;
. once nofill; flush left; boldfnt;
titulo
. normal
. ⊃
.
.macro references
. ⊂
. if lines<10 then skip to column 1 else skip 3;
. every heading (\\References\,,\\{PAGE}\)
. if hascontents then
. send contents
. ⊂
. checkskip;
. skip 1;
References→{page!}
. ⊃;
. once boldfnt; turn on "↓_"; <<not centering any more >>
. indent 0,0,0;
References
. normal
. ⊃
. << Spacing and Dialogue macros >>
.
.macro sp (n) << to set spacing to some number of mills >>
. ⊂ spacing n mills ⊃
.
.macro p (n) << to set preface to some number of mills >>
. ⊂ preface n mills ⊃
.
.macro spp(n,m) << to set spacing and preface in mills >>
. ⊂ sp n; p m; ⊃
.
.macro dial << for dialogue in times roman >>
. ⊂
. if lines<4 then next page else skip;
. begin "dial"
. indent 5,11;spp(30,80)
. ⊃;
.
.macro dialc
. ⊂
. skip;
. begin "dialcomment"
. indent 5,5; spp(30,80)
. ⊃
.
.macro endc
. ⊂
. end "dialcomment";
. ⊃
.
.macro endd
. ⊂
. end "dial";
. ⊃
.
.macro scenario
. ⊂
. begin nfnt; indent 5,5; spp 30,80;
. ⊃
. << ABSTRACT GENERATION >>
.
.macro abstract
. ⊂
. begin
. select D; << use \\foo\ for boldface >>
. indent 8,8,8
. spp(30,60)
. ⊃
.
.macro endabstract
. ⊂
. end;
. ⊃
. << GRAPHICS MACROS >>
.
.macro grfx ⊂
. begin "GRFX";
. group; nofill; spacing 0 mills; skip
. preface 0 mills; indent 0,0,0; grfxfnt;
. at "∂" ⊂ "αα" ⊃;
. at "∞" ⊂ "α%" ⊃; <<lado derecho de cajas>>
. turn off "←→↓_";
. ⊃
.
.macro gend ⊂
. skip;
. end "GRFX";
. ⊃
.
.macro caja (size)
. ⊂
. begin
. grfx;
. size2←(linewidth-size)/2;
. tabs size2, size2+size+1;
. boxsize ← size; << so fincaja knows what the size is >>
. turn on "\←";
. at "``" TXT "`" ⊂ "\~←%8TXT%7\~" ⊃ << en fix25 >>
. at "||" TXT "|" ⊂ "\~←%1TXT%7\~" ⊃ << en tim12s >>
\⊂{("∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂"[1 to size])}⊃
. ⊃
.
.macro fincaja
. ⊂
\α%{("∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂∂"[1 to boxsize])}$
. gend;
. end;
. ⊃
. << ACQMEM MACROS >>
.
.macro in
. ⊂
. i 5; << Used for standard indentation >>
. ⊃
.
.macro bi
. ⊂
. begin in; << used for indenting a block >>
. ⊃;
.
.macro i (x)
. ⊂
. indent x,x; << for indenting some number of spaces >>
. ⊃;
.
.macro bii
. ⊂
. begin << used for indenting 5 relative to current indent >>
. indent1←indent1+5; indent2←indent2+5;
. ⊃;
.
.macro off
. ⊂
. turn off "{"; << for set brackets >>
. ⊃
.
.macro bref
. ⊂
. begin indent 5,5; fixfnt; nofill; skip; group;
. ⊃
.
.<< Use the following macro for tree descriptors >>
.macro tree
. ⊂
. begin indent 5,5; fixfnt; nofill; skip;
. ⊃
. << INDENTATION CONTROL >>
.
.macro indenton ⊂ indent 4,0,0 ⊃
.macro indentoff ⊂ indent 0,0,0 ⊃
.
. << this macro for paragraphs that start with - >>
.macro dashp
. ⊂
. begin indent 5,7;spp 50,80
. ⊃
. << CONTENT MACROS >>
.
.macro gimmecontents
. ⊂
. hascontents ← true;
. ⊃
.
.macro putcontents
. ⊂
. contentspage←page+1;
. insert contents;
. portion main
. ⊃
.
.macro docontents
. ⊂
. count page from contentspage printing "i";
. next page;
. portion contents;
. every heading(,⊗⊗Table of Contents⊗,⊗⊗{page!}⊗)
. place heading;
. place text;
. nofill
. turn on "{#→";
. skip 4;
. preface 0;
. indent 0,0,0;
⊗⊗Section→Page⊗
. receive;
. ⊃
.
. macro checkskip
. ⊂
. if lines<3 then skip to column 1
. ⊃
.s Abstract
The proposed research is the second year of a research project on the
codification of concurrent program synthesis knowledge. The previous
proposal was a multi-year proposal, but has only received funding for the
first year. Accordingly, this proposal is an update of the first proposal
that includes a summary of the results obtained during part of the first
year.
The object of this research is to develop the knowledge base necessary for
the automatic synthesis of programs. The automatic synthesis of programs
allows improved performance in programming along the dimensions of design,
specification, coding, debugging, modification, documentation,
maintenance, reliability, cost, production time, handling of program
complexity, and ease of use by non-expert programmers, all problems of
major interest to the Air Force.
The thesis of the knowledge based approach to program synthesis is that
intelligent systems must contain and be able to use a great deal of
knowledge about the process of programming in order to effectively assist
the user in the many tasks necessary to achieve desired, effective
programs. Accordingly, the pacing item in this field is the codification
of programming knowledge in a form (usually rules) amenable to utilization
by computer programs. We have performed considerable codification of
programming knowledge and have
demonstrated the effectiveness of this approach by
implementing a series of systems embodying this knowledge. These
automatic synthesis systems were able
to successfully create sequential programs of moderate
complexity.
In the proposed research we plan to emphasize the codification of
programming knowledge for the area of concurrent programming. Practically
no work has been done on the automatic synthesis of concurrent programs,
yet the area is of critical importance for Air Force applications.
Examples include realtime control systems, distributed operating and
control systems, distributed data bases, concurrent signal processing algorithms,
and
target tracking algorithms.
We will study concurrent programming tasks and implement working synthesis
systems for a series of programming tasks of increasing complexity. In the
first year of this project, we studied the synthesis of concurrent versions
of several algorithms including sorting, set operations, shortest-path,
and simple distributed data base problems.
For these studies and from other research we performed recently, it appears
that in the second year we will develop a general formalism or framework
for the synthesis of concurrent algorithms. The basic idea is to use
a rich set of program transformations to generate a search space of
concurrent algorithms. This search will be guided toward algorithms that
match a particular target distributed hardware configuration. In another
application, system design, as exemplified by VLSI design, the search
for a suitable algorithm also allows the hardware configurations to be
generated to match the algorithm and data structures.
In addition to the practical payoff of this research, we expect to achieve
a contribution to science in the form of a theory, rather than an art, of
programming that will assist, not only in the automatic synthesis of
programs, but the teaching and understanding of the process of programming
and the understanding of the application of artificial intelligence to new
domains.
.S Overview and Relevance
The annual cost of software specification, development,
modification, documentation, and maintenance in the United States
is enormous.
The investment by the Air Force alone was over one billion dollars
in 1972 [Air Force-73, Boehm-73].
A significant portion of this cost is
spent in developing programs having a high degree of concurrency. The
purpose of the effort proposed herein is to codify the knowledge used in
developing concurrent programs. Once codified, this knowledge can be used
for for the development of an automatic programming system for concurrent
programs. This automation would significantly reduce DOD software costs.
We hope to demonstrate the feasibility of automatically generating
concurrent programs for military applications. The utility of the
automatic synthesis of programs will be demonstrated in terms of the total
time and cost to modify existing programs, the efficiency of the target
code and the program complexity manageable by the user. Examples shown in
this proposal illustrate some of the potential applications of the use of
knowledge based systems within the Air Force, but we feel that the benefit
is much higher than just these suggested applications. These applications
merely exemplify the benefit of a knowledge based programming system that
can, in a timely and correct manner, assist in the software areas of
.BEGIN NOFILL
.SINGLE SPACE
(1) design, in which the user decides what is wanted;
(2) specification, in which this intent is communicated to the computer;
(3) coding;
(4) debugging and testing;
(5) modification, in response to new needs or design requirements;
(6) documentation; and
(7) maintenance.
.END
The //Air Force Systems Command Research Planning Guide/ [Air Force-78]
states that one of their long-term objectives is automatic programming:
.bi
Research is needed in this area to develop practical systems that
automatically generate routine programs from a minimal input specification
or are able to automatically perform major modifications on existing
programs. Ultimate long-term orientation should be to handling inputs
from nonprofessional programmers in a loose-format, context-free
environment. Immediate results, understandably, will have more rigid
constraints. Current philosophy ties the principles of this field closely
with those of semiautomatic, assertion-oriented program verification.
However, an impasse as to the size of permitted programs appears likely;
as program size increases the theorems and proofs of the theorems grow
exponentially. Therefore, alternate methods to those that currently exist
are necessary for automatically generating and proving theorems for
large-scale programs. Also, for the automatic generation of programs,
research is needed in theoretically defining and specifying the semantics
of data and the semantic operation of computer programs.
.end
The work we are proposing is oriented toward the Air Force's programming
objective in the important domain of concurrent systems. Concurrency is
exploited heavily in the most complex programs in existence, including
advanced operating systems, computer networks, avionics systems, weapons
control, and target control and tracking. This work therefore has
substantial value.
One very important use of the work we are proposing is in synthesis of
realtime control programs for on-board computers on airplanes. Such
programs require concurrency, so that our synthesis knowledge pertaining
to concurrency would play a major role in their automatic synthesis.
Another important use of this program synthesis system is for the
modification or extension of a signal understanding system operating in a
dynamically changing environment. Signal understandin